perm filename ARPA[S79,JMC] blob
sn#437482 filedate 1979-04-30 generic text, type C, neo UTF8
COMMENT ā VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 McCarthy has recently discovered a new language called Elephant
C00008 ENDMK
Cā;
McCarthy has recently discovered a new language called Elephant
for writing sequential programs. It has two interesting properties.
First, the programs are represented as collections of sentences of first
order logic. In this respect Elephant resembles Lucid and Prolog.
However, the Elephant representation is more direct than these and permits
proving properties of the program without any special mathematical theory
of computation - merely the program itself and an axiomatization of the
data domain. The method involves replacing each variable of the program
and the "program counter" by a function of time and writing recursion
equations for this function.
The Elephant style of describing algorithms is in some sense the
opposite of the method of describing recursive programs due to Cartwright
and developed by Cartwright and McCarthy (1978, 1979). Namely, the
recursive function method describes the output function in terms of
simpler cases and therefore can be called %2top-down%1, while the Elephant
method works from an initial state and desribes how it is transformed.
Presumably the two methods will be found to be complementary.
The second property of Elephant makes it a higher level
language than any in present use at the cost of requiring a heuristic
program as a compiler. Namely, an Elephant statement can refer to
the past without specifying any data structure in which information
about the past is stored. As an informal example, an Elephant program
can say, %2"A passenger has a reservation if he has successfully made
one and hasn't cancelled it"%1. The point is that the program prescribes
no data structure for remembering reservations, and the compiler must
decide that cancelled reservations and unsuccessful attempts to make
reservations do not have to be remembered. It seems to us that the
italicized statement is one that is likely to be made by a person
describing in English what he wants a computer to do. Unless he
is a programmer, it may not even occur to him that some data
structure must be created and maintained in order to get the desired
behavior.
Elephant programs that refer to the past in this way are
nevertheless collections of sentences of logic, and their properties
can be stated and proved without an additional theory of computation.
Concurrent processes can also be described in Elephant. In particular,
the fact of non-interference of processes can be specified without
giving a method of achieving it, thus leaving achieving non-interference
up to the compiler.
More sample programs need to be written before it can be
determined whether Elephant or Elephant features are a convenient
way of writing programs. If the answer to this question is positive,
the next step is the design of a compiler. Since the design of
data structures will probably turn out to be a substantial mathematical
problem in general, an Elephant compiler will be a heuristic program
that recognizes certain cases and doesn't always give an acceptable
result without the help of putting in some data structures explicitly.
Before this it may be desirable to gain some experience in
transforming Elephant programs mathematically, e.g. in transforming
programs that refer to the distant past into programs that refer
only to the immediate past but in which data structures are explicit.
A preliminary writeup on Elephant is included as Appendix A.